Definitions | False, P  Q, A, t T, x:A. B(x),  b, , s = t, Prop, Type, x.A(x),  x. t(x), f(x), Top, a:A fp B(a), x:A B(x), x:A B(x), P & Q, P  Q, Unit, left+right, f(x)?z, P  Q, @loc x initially v:T, {x:A| B(x) }, (x l), Realizer, fpf-domain(f), x L.R(x), State(ds), @loc precondition for a(v:T):P State(ds) v, left right, R-pre-init(i;ds;init;a;T;P), IdDeq, x dom(f), b, Id |